\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. Dec($P$($e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\exists$${\it e'}$:E. ((${\it e'}$ $<$ $e$) \& $P$(${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. ((${\it e'}$ $<$ $e$) \& $P$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e'}$ $<$ ${\it e''}$) $\Rightarrow$ (${\it e''}$ $<$ $e$) $\Rightarrow$ ($\neg$$P$(${\it e''}$))))))
\-
\end{tabbing}